+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
-1(s(x), s(y)) → -1(x, y)
IFFACT(x, true) → -1(x, s(0))
FACT(x) → GE(x, s(s(0)))
+1(x, s(y)) → +1(x, y)
FACT(x) → IFFACT(x, ge(x, s(s(0))))
*1(x, s(y)) → *1(x, y)
GE(s(x), s(y)) → GE(x, y)
IFFACT(x, true) → FACT(-(x, s(0)))
*1(x, s(y)) → +1(*(x, y), x)
IFFACT(x, true) → *1(x, fact(-(x, s(0))))
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
-1(s(x), s(y)) → -1(x, y)
IFFACT(x, true) → -1(x, s(0))
FACT(x) → GE(x, s(s(0)))
+1(x, s(y)) → +1(x, y)
FACT(x) → IFFACT(x, ge(x, s(s(0))))
*1(x, s(y)) → *1(x, y)
GE(s(x), s(y)) → GE(x, y)
IFFACT(x, true) → FACT(-(x, s(0)))
*1(x, s(y)) → +1(*(x, y), x)
IFFACT(x, true) → *1(x, fact(-(x, s(0))))
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
-1(s(x), s(y)) → -1(x, y)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
-1(s(x), s(y)) → -1(x, y)
The value of delta used in the strict ordering is 1.
POL(-1(x1, x2)) = x_2
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GE(s(x), s(y)) → GE(x, y)
The value of delta used in the strict ordering is 1.
POL(GE(x1, x2)) = x_2
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
+1(x, s(y)) → +1(x, y)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(x, s(y)) → +1(x, y)
The value of delta used in the strict ordering is 1/16.
POL(s(x1)) = 1/4 + (2)x_1
POL(+1(x1, x2)) = (1/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
*1(x, s(y)) → *1(x, y)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(x, s(y)) → *1(x, y)
The value of delta used in the strict ordering is 1/16.
POL(*1(x1, x2)) = (1/4)x_2
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
FACT(x) → IFFACT(x, ge(x, s(s(0))))
IFFACT(x, true) → FACT(-(x, s(0)))
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)